globalvar tickNum=0

The above defines a global variable tickNum, which is used to record the number of continuous "tick".

def metronome(t) = signal | Rtimer(t) >> metronome(t)

The above defines a metronome where it publishes signal every t time unit.

  metronome(1000) >> $GUpdate({tickNum=tickNum+1}) >> "tick"
      | Rtimer(500) >> metronome(1000) >> $GUpdate({tickNum=tickNum-1}) >>"tock"

The above publishes "tick" once per second, and publishes "tock" once per second after an intial half-second delay. Thus the publications are "tick tock tick ... " where "tick" and "tock" alternate each other.

#define consecutiveTickOrTock (tickNum < 0 || tickNum > 1)

The above defines a condition named as consecutiveTickOrTock which represents the condition such that tickNum is either smaller than 0 or larger than 1.

#assert System deadlockfree;

The above checks whether the system is deadlock-free.

#assert System |= []<>"tick" && []<>"tock";

The above checks whether the system can always eventually publish "tick" and always eventually publish "tock".

#assert System |= []!consecutiveTickOrTock;

The above checks that whether the system always not satisfies the condition specified by consecutiveTickOrTock.

#assert System reaches consecutiveTickOrTock;

The above checks that whether the system can reaches the condition specified by consecutiveTickOrTock.